es:ES, ff:FIFO, f2f+:F2F+-decls.
plus-ify{i:l}(es;ff;is_req  ;is_ack ;awaiting ;owes_ack )
 (sndr, rcvr:ff.C, e, e':E.
 ([e: sndr is_req   rcvr]  [e: rcvr is_ack  sndr])
  ([e': sndr is_req   rcvr]  [e': rcvr is_ack  sndr])
  ((e < e')  (f2f+-p+(e,e')))) 

latex

Definitions	x:A. B(x), FIFO, F2F+-decls, P  Q, P & Q, t  T, A c B, , P  Q, x(s), P  Q, P  Q, {T}, f2f+-p+
Lemmas	f2f+-property, plus-ify wf, es-E wf, Id wf, fifoC wf, es-dtype wf, bool wf, fifoR wf, es-loc wf, decidable wf, fifoS wf, not wf, snd-it wf, top wf, es-state wf, fifo wf, event system wf, f2f+-pred-generates-thread, generated-thread-properties2, f2f+-pred wf, f2f+-pred-field, es-causl wf, f2f+-p+ wf